pred!(e;e') == (((first(e'))) c (e = pred(e')))  ((rcv?(e')) c (e = sender(e'))) 

latex

---

clarification:

pred!(E;pred?;info;e;e')
== (((first(pred?;e'))) c (e = pred(pred?;e')  E))
==  ((rcv?(info;e')) c (e = sender(info;e')  E)) 

latex

Definitions	pred!(e;e'), P  Q, A, first(e), pred(e), A c B, b, rcv?(e), sender(e)
FDL editor aliases	pred!